Nuprl Lemma : isrcv_wf
11,40
postcript
pdf
k
:Knd. isrcv(
k
)
latex
Definitions
x
:
A
.
B
(
x
)
,
Knd
,
t
T
,
isrcv(
k
)
Lemmas
isl
wf
,
IdLnk
wf
,
Id
wf
origin
k:Knd. isrcv(k) 
k:Knd. isrcv(k) x:A. B(x) T